Calculus of Inductive Constructions
https://coq.inria.fr/refman/language/cic.html
Coq
の
型システム
https://en.wikipedia.org/wiki/Calculus_of_constructions